P1, P2, Q1, Q2:. (P1  P2)  (Q1  Q2)  ((P1 & Q1)  (P2 & Q2)) 

latex

ProofTree

Definitions	t  T, P  Q, P & Q, P  Q, P  Q, , x:A. B(x)
Lemmas	iff wf